(declare-const v0 Bool)
(declare-const r1 Real)
(declare-const r5 Real)
(declare-const r7 Real)
(declare-const r8 Real)
(declare-const r12 Real)
(declare-const v1 Bool)
(declare-const v2 Bool)
(assert (not (exists ((q3 Real) (q4 Bool) (q5 Bool) (q6 Bool)) (=> (not q4) (> r1 q3 8.0)))))
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v7 Bool)
(declare-const r13 Real)
(assert (exists ((q20 Real) (q21 Real) (q22 Bool) (q23 Real)) v5))
(declare-const v8 Bool)
(declare-const v12 Bool)
(assert (or (not v5) v8 v12))
(assert (or (> 9529954577.0 r1 r13) (> 9529954577.0 r1 r13) (or v5 v4 v1 (>= 9529954577.0 r12) v2 (>= 9529954577.0 r12) (>= 56081222690.0 0.7037 r7 r5 0.7037) v0 v0 (>= 56081222690.0 0.7037 r7 r5 0.7037)) (< 0.7037 0.7037 0.7037 r8) v8))
(check-sat)
